Iof proof for Lemma decidable or:
1. P :
2. Q :
3.
P
4. Q
(P 
Q) ((P Q))
by ((((DNth 1 0)
CollapseTHENM (DNth 2 0))
)
CollapseTHEN ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))
C.| 9,38 |
P
(P Q) ((P Q))
by ((((DNth 1 0)
CollapseTHENM (DNth 2 0)))
CollapseTHEN ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))
C.
| Definitions |  T Q x:A. B(x) |
| Lemmas |